Skip to content

feat(CFG): Verified implementation of Kildall's algorithm - #782

Draft
quartztz wants to merge 10 commits into
leanprover:mainfrom
quartztz:qtz/kildall
Draft

feat(CFG): Verified implementation of Kildall's algorithm#782
quartztz wants to merge 10 commits into
leanprover:mainfrom
quartztz:qtz/kildall

Conversation

@quartztz

@quartztz quartztz commented Aug 7, 2026 •
edited
Loading

Copy link
Copy Markdown

As discussed on Zulip, here is an implementation of Kildall's worklist algorithm for solving dataflow equations. The design features a small CFG api, as well as a characterization of correctness in terms of different flavors of fixpoints. Three main theorems show that

  • The result of the algorithm is a postfixpoint (valid solution)
  • If the transfer functions are monotone, the postfixpoint that is computed is the least postfixpoint
  • If the transfer functions are monotone, the result is a fixpoint

Definitions of the structures are in Analysis/Dataflow/CFG.lean, and the algorithm and proofs are in Analysis/Dataflow/Kildall.lean. I didn't feel like it fit semantically in any other directory, but I'll be glad to move it if there's better.

TODO: fix all lints :(

@quartztz
quartztz marked this pull request as draft August 7, 2026 16:07
ctchou
ctchou reviewed Aug 7, 2026
View reviewed changes

@ctchou ctchou left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@fmontesi Do you have any opinions about the placement of these files?

Comment thread Cslib/Analysis/Dataflow/Kildall.lean
Comment on lines +38 to +40
* [G. Kildall, *A Unified Approach to Global Program Optimization*][Kildall73]
* [F. Nielson, H.R. Nielson, C. Hankin, *Principles of Program Analysis*][Nielson99]
* [R. LaSpina, *Formal Verification of WTO-based Dataflow Solvers*][LaSpina25]

@ctchou ctchou Aug 7, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Please add these references to the file references.bib.

ctchou
ctchou reviewed Aug 8, 2026
View reviewed changes
Comment thread Cslib/Analysis/Dataflow/CFG.lean Outdated
Comment on lines +27 to +44
/-- Abstract structure defining the necessary operations on a CFG to define a Control Flow Graph. -/
class CFG (Node Edge : Type) [DecidableEq Node] [DecidableEq Edge] where
/-- All of the nodes in the CFG. -/
nodes : List Node
/-- All of the edges in the CFG. -/
edges : List Edge
/-- A distinguished entry node in the CFG. -/
entry : Node
/-- A proof that the entry node is part of the graph's nodes. -/
entry_mem : entry ∈ nodes
/-- Extractor function for an edge's source node. -/
_srcOf : Edge → Node
/-- Proof of correctness for the source extractor. -/
srcOf_mem : ∀ e ∈ edges, _srcOf e ∈ nodes
/-- Extractor function for an edge's destination node. -/
_dstOf : Edge → Node
/-- Proof of correctness for the destination extractor. -/
dstOf_mem : ∀ e ∈ edges, _dstOf e ∈ nodes

@ctchou ctchou Aug 8, 2026 •
edited
Loading

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I have some questions about the design of CFG:

  • Normally the nodes and edges of a graph are taken to be sets (which can be modeled by Set or Finset). Why do you define them to be lists and then build types from them (NodeOf and EdgeOf)? Scanning the code in Kildall.lean, I'm not sure you ever used the fact that nodes and edges are lists (rather than sets).
  • For that matter, do you really need the generality that nodes and edges are subsets of Node and Edge. Can they simply be the whole types? Then you won't need constraints like setOf_mem and dstOf_mem.
  • There is something called Quiver in mathlib:
    https://leanprover-community.github.io/mathlib4_docs/Mathlib/Combinatorics/Quiver/Basic.html
    Would it usable for your purpose?
  • Why did you put _ at the beginning of _srcOf and dstOf?

@quartztz quartztz Aug 8, 2026

Copy link
Copy Markdown
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I agree with the fact that the current presentation is very roundabout. I did not know about Quiver, but I feel like applying it would fix these comments: using a single type for Nodes and a quiver to characterize the edges would both remove unneeded fields and make the projections easier.

The _ was a crude way to mark that field as "internal", since the preferred API (that returns a NodeOf g) is defined in terms of it. However, this problem disappears when applying the other changes, so i'll draft a new structure to hopefully fix everything in one go.

Thank you for your comments and for the pointer!

@quartztz

quartztz commented Aug 10, 2026

Copy link
Copy Markdown
Author

Second try, integrating the previous comments regarding the type of Node, and using Quiver for edges.

While the definition of the CFG using Finsets is definitely simpler, I really wanted to keep the algorithm computable, and one way I found is to add a linear order on the nodes of the CFG. This "workaround" is relatively inobtrusive (any instantiation can supply a unique id : Nat field for Nodes and give an "arbitrary" order based on that), as well as potentially useful for the definition of alternate scheduling strategies on the algorithm, for optimization (not as of right now, it would require some adaptation to the structure and the algorithm I haven't given enough deep thought to yet).

My question is therefore the following: what's the project's stance on computability?

I'm not a huge fan of this workaround, but I cannot see a way to make computability work without it. I having a noncomputable algorithm is a shame, but that means that either the CFG structure carries Lists (and is ugly) or we do this sort of workaround (which is also ugly, on the same level as lists in my opinion).

If the library doesn't care about the algorithm being computable, then the Finset formulation can be used without issues, and I'll be glad (if a bit heartbroken) to rewrite everything in a noncomputable manner.

ctchou
ctchou requested changes Aug 10, 2026
View reviewed changes

@ctchou ctchou left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Your patch produced a very large diff on references.bib which obscures the change you actually made. Could you revert it and make your small change manually? We are not against reformatting references.bib, but that should be done in a separate PR and not be mixed with this PR.

@quartztz

quartztz commented Aug 10, 2026

Copy link
Copy Markdown
Author

That's my bad, the autoformatter kicked in. Pushed a commit to fix! Sorry about that.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@ctchou ctchou ctchou requested changes
@fmontesi fmontesi Awaiting requested review from fmontesi fmontesi is a code owner
@chenson2018 chenson2018 Awaiting requested review from chenson2018 chenson2018 is a code owner

Requested changes must be addressed to merge this pull request.

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@quartztz @ctchou